1. Technical Field
The present disclosure generally relates to verification techniques for integrated circuit logic design and in particular to techniques for performing counterexample-guided proof-based abstractions.
2. Description of the Related Art
Formal verification techniques are powerful tools for the construction of correct logic designs. These verification techniques have the power to expose even the most probabilistically uncommon scenario that may result in a functional design failure, and ultimately, the techniques have the power to prove that the design is correct, i.e., that no failing scenario exists. Unfortunately, formal verification techniques require computational resources, and these computational resources are exponential with respect to the size of the design under test, requiring, in a worst case scenario, the analysis of every “reachable state” of a given design. Various techniques have been proposed to enable application of formal verification techniques to large designs, and most of these techniques rely on the technique of Abstraction.